(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x2684ee632a1e15d5) #x0000000024231110))
(constraint (= (f #x67128e6921e0b217) #x9c4a39a48782c85a))
(constraint (= (f #x8a394b43109c6a92) #x28e52d0c4271aa4a))
(constraint (= (f #x52948738a9ab7875) #x0000000084200145))
(constraint (= (f #x80e9824d8eb4145a) #x03a609363ad0516a))
(constraint (= (f #xe30de883e344aeea) #x8c37a20f8d12bbaa))
(constraint (= (f #x982940eb9032de77) #x60a503ae40cb79da))
(constraint (= (f #x483c5e9b56495e54) #x0000000040e0d092))
(constraint (= (f #xe72a23533bb0ea15) #x0000000111101899))
(constraint (= (f #xebdce65a2e5b04eb) #xaf739968b96c13aa))
(constraint (= (f #xe79e998e84ec73a3) #x9e7a663a13b1ce8a))
(constraint (= (f #x62c2cb69a69e2732) #x8b0b2da69a789cca))
(constraint (= (f #xa339b1a811ca8513) #x8ce6c6a0472a144a))
(constraint (= (f #x4da550be0795cae0) #x0000000028008030))
(constraint (= (f #xb4ad9aebeeed480e) #xd2b66bafbbb5203a))
(constraint (= (f #x14056c3e874941a6) #x5015b0fa1d25069a))
(constraint (= (f #xee3eab537e6126ea) #xb8faad4df9849baa))
(constraint (= (f #x6c5dd3853e895163) #xb1774e14fa25458a))
(constraint (= (f #x8d354d3047444973) #x34d534c11d1125ca))
(constraint (= (f #x56247a9987165e3c) #x000000002100c408))
(constraint (= (f #x563e500625728e97) #x58f9401895ca3a5a))
(constraint (= (f #x02da063c90a9b2b0) #x0000000010102084))
(constraint (= (f #x2861006e4d979836) #xa18401b9365e60da))
(constraint (= (f #xb4b92d58d52b6532) #xd2e4b56354ad94ca))
(constraint (= (f #xd60085348d7e9eda) #x580214d235fa7b6a))
(constraint (= (f #xea98165976586309) #x0000000440808282))
(constraint (= (f #x41aab6d43e2a33c2) #x06aadb50f8a8cf0a))
(constraint (= (f #x217bc2d4b5cd5056) #x85ef0b52d735415a))
(constraint (= (f #x51ee8ee93a7b3873) #x47ba3ba4e9ece1ca))
(constraint (= (f #x76929ebd83191c32) #xda4a7af60c6470ca))
(constraint (= (f #x21a39ec77023c0cc) #x000000010c143201))
(constraint (= (f #xe4b295e919e1ce54) #x0000000504840848))
(constraint (= (f #x89a65d2b3c82e731) #x0000000400204940))
(constraint (= (f #xb3c4e79b8c313e7e) #xcf139e6e30c4f9fa))
(constraint (= (f #xe017ccb088c5a634) #x0000000000240404))
(constraint (= (f #xa186ed3330a1c15a) #x861bb4ccc287056a))
(constraint (= (f #x2eddb71b4612dab2) #xbb76dc6d184b6aca))
(constraint (= (f #x1543394ebb195e3a) #x550ce53aec6578ea))
(constraint (= (f #x4531789664b2129c) #x0000000009808021))
(constraint (= (f #x836d352c25e7e9c5) #x0000000009292121))
(constraint (= (f #x7b20d2e8a989273b) #xec834ba2a6249cea))
(constraint (= (f #xa3864dd5b96d76eb) #x8e193756e5b5dbaa))
(constraint (= (f #xbe7e03e16ce30424) #x00000001f0100b03))
(constraint (= (f #x9967d8ecae07d9ae) #x659f63b2b81f66ba))
(constraint (= (f #xd6955481220ee63b) #x5a555204883b98ea))
(constraint (= (f #xb71e475403cead58) #x00000000b0322000))
(constraint (= (f #x7357dba5eb088ee5) #x000000029a9c0d08))
(constraint (= (f #x69706bb155be53b3) #xa5c1aec556f94eca))
(constraint (= (f #xd54ce7e888e97194) #x0000000222270444))
(constraint (= (f #x014237e365e11ede) #x0508df8d97847b7a))
(constraint (= (f #x86100d17288705e3) #x1840345ca21c178a))
(constraint (= (f #x0a0454bd9073a737) #x281152f641ce9cda))
(constraint (= (f #x3a3a6e8cb1488869) #x00000001d1506400))
(constraint (= (f #x38789398b55e1eee) #xe1e24e62d5787bba))
(constraint (= (f #x1d621e6d8391678c) #x000000000010600c))
(constraint (= (f #x249364e0c88cc2c9) #x0000000000030604))
(constraint (= (f #x4e636765ee20c67c) #x00000002131b2b21))
(constraint (= (f #x154144bb08809ed6) #x550512ec22027b5a))
(constraint (= (f #xd895e8eb2ac4aadc) #x0000000484074150))
(constraint (= (f #xec791e3a866580a5) #x0000000340c0d010))
(constraint (= (f #xded04b3de971e004) #x000000068200494b))
(constraint (= (f #x443aa596e44e9566) #x10ea965b913a559a))
(constraint (= (f #x42a5d964c05d256e) #x0a976593017495ba))
(constraint (= (f #x95d56175c4809ac7) #x575585d712026b1a))
(constraint (= (f #x06eae0286169c92d) #x0000000017010103))
(constraint (= (f #xe57eed985c6d15d6) #x95fbb66171b4575a))
(constraint (= (f #x39cdd7bdeaa5e4ec) #x000000004e2cad45))
(constraint (= (f #x4658e354abe6cee4) #x0000000202020005))
(constraint (= (f #x13400e918c43001e) #x4d003a46310c007a))
(constraint (= (f #x72e6e1cb659e1c26) #xcb9b872d9678709a))
(constraint (= (f #xeb82050c62e8d36e) #xae0814318ba34dba))
(constraint (= (f #x4d329e0d7cd6c200) #x0000000000906062))
(constraint (= (f #xe7c70194772dd15e) #x9f1c0651dcb7457a))
(constraint (= (f #x70d0a8c8ea42ae78) #x0000000284044642))
(constraint (= (f #xea771a7d1a8bc952) #xa9dc69f46a2f254a))
(constraint (= (f #xcec4588e07dc278e) #x3b1162381f709e3a))
(constraint (= (f #x2d22d9eb1424c329) #x0000000100064800))
(constraint (= (f #x8797edae374e5dba) #x1e5fb6b8dd3976ea))
(constraint (= (f #x5073347d0356dd32) #x41ccd1f40d5b74ca))
(constraint (= (f #x9c6e7793ac11e438) #x0000000063309c00))
(constraint (= (f #x169ce18d261e3beb) #x5a7386349878efaa))
(constraint (= (f #xe28b99097beb41d8) #x000000041448484b))
(constraint (= (f #xd078b27e1c535dd9) #x00000002818190e0))
(constraint (= (f #x526ec8b69c53eb4e) #x49bb22da714fad3a))
(constraint (= (f #x03dd8e3e438abb22) #x0f7638f90e2aec8a))
(constraint (= (f #xa7a9695dc00e31e6) #x9ea5a5770038c79a))
(constraint (= (f #x53eb02e00353ab73) #x4fac0b800d4eadca))
(constraint (= (f #xe367aa3750541ed1) #x0000000319111082))
(constraint (= (f #x5cd0c2998ec15246) #x73430a663b05491a))
(constraint (= (f #xc490597adb3bceb5) #x000000040082c2d0))
(constraint (= (f #x5e64cb1d625e4ce9) #x0000000222004802))
(constraint (= (f #x9346914bc6470571) #x0000000010000a12))
(constraint (= (f #x4ea6363772603418) #x000000003131b193))
(constraint (= (f #xd8ae831515ed73c6) #x62ba0c5457b5cf1a))
(constraint (= (f #xcc71eebc42eb8b15) #x0000000203056002))
(constraint (= (f #xc7b71c272c1ead09) #x0000000438a02120))
(constraint (= (f #xa999ac95a97ece16) #xa666b256a5fb385a))
(constraint (= (f #x45924cea15690651) #x0000000000024000))
(constraint (= (f #x85a579006050122c) #x0000000429080002))
(constraint (= (f #xaece1ab45d6d0dde) #xbb386ad175b4377a))
(check-synth)
